<!DOCTYPE html>



  


<html class="theme-next mist use-motion" lang="">
<head><meta name="generator" content="Hexo 3.8.0">
  <meta charset="UTF-8">
<meta http-equiv="X-UA-Compatible" content="IE=edge">
<meta name="viewport" content="width=device-width, initial-scale=1, maximum-scale=1">
<meta name="theme-color" content="#222">



  
  
    
    
  <script src="/lib/pace/pace.min.js?v=1.0.2"></script>
  <link href="/lib/pace/pace-theme-minimal.min.css?v=1.0.2" rel="stylesheet">







<meta http-equiv="Cache-Control" content="no-transform">
<meta http-equiv="Cache-Control" content="no-siteapp">
















  
  
  <link href="/lib/fancybox/source/jquery.fancybox.css?v=2.1.5" rel="stylesheet" type="text/css">







<link href="/lib/font-awesome/css/font-awesome.min.css?v=4.6.2" rel="stylesheet" type="text/css">

<link href="/css/main.css?v=5.1.4" rel="stylesheet" type="text/css">


  <link rel="apple-touch-icon" sizes="180x180" href="/images/apple-touch-icon-next.png?v=5.1.4">


  <link rel="icon" type="image/png" sizes="32x32" href="/images/favicon-32x32-next.png?v=5.1.4">


  <link rel="icon" type="image/png" sizes="16x16" href="/images/favicon-16x16-next.png?v=5.1.4">


  <link rel="mask-icon" href="/images/logo.svg?v=5.1.4" color="#222">





  <meta name="keywords" content="系统总结,">










<meta name="description" content="本文首发于：安恒讲武堂 前几天在群里看到有人聊到z3，正好在寒假的时候仔细研究过这个模块，今天就和大家分享下z3的简易使用方法和在ctf中该模块对于求解逆向题的帮助 简介z3z3是由微软公司开发的一个优秀的SMT求解器，它能够检查逻辑表达式的可满足性，通俗的来讲我们可以简单理解为它是一个解方程的计算器 SMTSMT即可满足性模理论，它是对一个实际问题求解的特征描述，这些特征就是我们所求解的特征，S">
<meta name="keywords" content="系统总结">
<meta property="og:type" content="article">
<meta property="og:title" content="Z3简介及在逆向领域的应用">
<meta property="og:url" content="https://yml-sec.top/2019/04/14/Z3简介及在逆向领域的应用/index.html">
<meta property="og:site_name" content="yemoli&#39;s blog">
<meta property="og:description" content="本文首发于：安恒讲武堂 前几天在群里看到有人聊到z3，正好在寒假的时候仔细研究过这个模块，今天就和大家分享下z3的简易使用方法和在ctf中该模块对于求解逆向题的帮助 简介z3z3是由微软公司开发的一个优秀的SMT求解器，它能够检查逻辑表达式的可满足性，通俗的来讲我们可以简单理解为它是一个解方程的计算器 SMTSMT即可满足性模理论，它是对一个实际问题求解的特征描述，这些特征就是我们所求解的特征，S">
<meta property="og:locale" content="default">
<meta property="og:image" content="https://i.loli.net/2019/04/06/5ca80a3429c22.jpg">
<meta property="og:image" content="https://i.loli.net/2019/04/06/5ca80aced6bf2.jpg">
<meta property="og:image" content="https://i.loli.net/2019/04/06/5ca80d2aac914.jpg">
<meta property="og:image" content="https://i.loli.net/2019/04/06/5ca810dd35daf.jpg">
<meta property="og:image" content="https://i.loli.net/2019/04/06/5ca8138baa122.jpg">
<meta property="og:image" content="https://i.loli.net/2019/04/06/5ca81401ead52.jpg">
<meta property="og:image" content="https://i.loli.net/2019/04/06/5ca81ccc941ff.jpg">
<meta property="og:image" content="https://i.loli.net/2019/04/06/5ca82e010c4ae.jpg">
<meta property="og:image" content="https://i.loli.net/2019/04/06/5ca82ffb172a5.jpg">
<meta property="og:image" content="https://i.loli.net/2019/04/06/5ca83192d0a23.jpg">
<meta property="og:image" content="https://i.loli.net/2019/04/06/5ca8328b64699.jpg">
<meta property="og:image" content="https://i.loli.net/2019/04/06/5ca834ef90a97.jpg">
<meta property="og:image" content="https://i.loli.net/2019/04/06/5ca8395b629d4.jpg">
<meta property="og:image" content="https://i.loli.net/2019/04/06/5ca839bde9e02.jpg">
<meta property="og:updated_time" content="2019-04-14T12:50:42.199Z">
<meta name="twitter:card" content="summary">
<meta name="twitter:title" content="Z3简介及在逆向领域的应用">
<meta name="twitter:description" content="本文首发于：安恒讲武堂 前几天在群里看到有人聊到z3，正好在寒假的时候仔细研究过这个模块，今天就和大家分享下z3的简易使用方法和在ctf中该模块对于求解逆向题的帮助 简介z3z3是由微软公司开发的一个优秀的SMT求解器，它能够检查逻辑表达式的可满足性，通俗的来讲我们可以简单理解为它是一个解方程的计算器 SMTSMT即可满足性模理论，它是对一个实际问题求解的特征描述，这些特征就是我们所求解的特征，S">
<meta name="twitter:image" content="https://i.loli.net/2019/04/06/5ca80a3429c22.jpg">



<script type="text/javascript" id="hexo.configurations">
  var NexT = window.NexT || {};
  var CONFIG = {
    root: '/',
    scheme: 'Mist',
    version: '5.1.4',
    sidebar: {"position":"left","display":"post","offset":12,"b2t":false,"scrollpercent":false,"onmobile":false},
    fancybox: true,
    tabs: true,
    motion: {"enable":true,"async":false,"transition":{"post_block":"fadeIn","post_header":"slideDownIn","post_body":"slideDownIn","coll_header":"slideLeftIn","sidebar":"slideUpIn"}},
    duoshuo: {
      userId: '0',
      author: 'Author'
    },
    algolia: {
      applicationID: '',
      apiKey: '',
      indexName: '',
      hits: {"per_page":10},
      labels: {"input_placeholder":"Search for Posts","hits_empty":"We didn't find any results for the search: ${query}","hits_stats":"${hits} results found in ${time} ms"}
    }
  };
</script>



  <link rel="canonical" href="https://yml-sec.top/2019/04/14/Z3简介及在逆向领域的应用/">





  <title>Z3简介及在逆向领域的应用 | yemoli's blog</title>
  








</head>

<body itemscope="" itemtype="http://schema.org/WebPage" lang="default">

  
  
    
  

  <div class="container sidebar-position-left page-post-detail">
    <div class="headband"></div>
    <header id="header" class="header" itemscope="" itemtype="http://schema.org/WPHeader">
      <div class="header-inner"><div class="site-brand-wrapper">
  <div class="site-meta ">
    

    <div class="custom-logo-site-title">
      <a href="/" class="brand" rel="start">
        <span class="logo-line-before"><i></i></span>
        <span class="site-title">yemoli's blog</span>
        <span class="logo-line-after"><i></i></span>
      </a>
    </div>
      
        <p class="site-subtitle"></p>
      
  </div>

  <div class="site-nav-toggle">
    <button>
      <span class="btn-bar"></span>
      <span class="btn-bar"></span>
      <span class="btn-bar"></span>
    </button>
  </div>
</div>

<nav class="site-nav">
  

  
    <ul id="menu" class="menu">
      
        
        <li class="menu-item menu-item-home">
          <a href="/" rel="section">
            
              <i class="menu-item-icon fa fa-fw fa-home"></i> <br>
            
            Home
          </a>
        </li>
      
        
        <li class="menu-item menu-item-about">
          <a href="/about/" rel="section">
            
              <i class="menu-item-icon fa fa-fw fa-user"></i> <br>
            
            About
          </a>
        </li>
      
        
        <li class="menu-item menu-item-tags">
          <a href="/tags/" rel="section">
            
              <i class="menu-item-icon fa fa-fw fa-tags"></i> <br>
            
            Tags
          </a>
        </li>
      
        
        <li class="menu-item menu-item-archives">
          <a href="/archives/" rel="section">
            
              <i class="menu-item-icon fa fa-fw fa-archive"></i> <br>
            
            Archives
          </a>
        </li>
      
        
        <li class="menu-item menu-item-friends">
          <a href="/friends/" rel="section">
            
              <i class="menu-item-icon fa fa-fw fa-sitemap"></i> <br>
            
            friends
          </a>
        </li>
      

      
    </ul>
  

  
</nav>



 </div>
    </header>

    <main id="main" class="main">
      <div class="main-inner">
        <div class="content-wrap">
          <div id="content" class="content">
            

  <div id="posts" class="posts-expand">
    

  

  
  
  

  <article class="post post-type-normal" itemscope="" itemtype="http://schema.org/Article">
  
  
  
  <div class="post-block">
    <link itemprop="mainEntityOfPage" href="https://yml-sec.top/2019/04/14/Z3简介及在逆向领域的应用/">

    <span hidden itemprop="author" itemscope="" itemtype="http://schema.org/Person">
      <meta itemprop="name" content="夜莫离、">
      <meta itemprop="description" content="">
      <meta itemprop="image" content="/images/avatar.gif">
    </span>

    <span hidden itemprop="publisher" itemscope="" itemtype="http://schema.org/Organization">
      <meta itemprop="name" content="yemoli's blog">
    </span>

    
      <header class="post-header">

        
        
          <h1 class="post-title" itemprop="name headline">Z3简介及在逆向领域的应用</h1>
        

        <div class="post-meta">
          <span class="post-time">
            
              <span class="post-meta-item-icon">
                <i class="fa fa-calendar-o"></i>
              </span>
              
                <span class="post-meta-item-text">Posted on</span>
              
              <time title="Post created" itemprop="dateCreated datePublished" datetime="2019-04-14T20:48:25+08:00">
                2019-04-14
              </time>
            

            

            
          </span>

          

          
            
          

          
          

          

          
            <div class="post-wordcount">
              
                
                <span class="post-meta-item-icon">
                  <i class="fa fa-file-word-o"></i>
                </span>
                
                  <span class="post-meta-item-text">Words count in article&#58;</span>
                
                <span title="Words count in article">
                  2.2k
                </span>
              

              
                <span class="post-meta-divider">|</span>
              

              
                <span class="post-meta-item-icon">
                  <i class="fa fa-clock-o"></i>
                </span>
                
                  <span class="post-meta-item-text">Reading time &asymp;</span>
                
                <span title="Reading time">
                  9
                </span>
              
            </div>
          

          

        </div>
      </header>
    

    
    
    
    <div class="post-body" itemprop="articleBody">

      
      

      
        <p>本文首发于：<a href="安恒讲武堂" title="https://mp.weixin.qq.com/s/GKbxGaWcBPfEuBGtWQ3uNw">安恒讲武堂</a></p>
<p>前几天在群里看到有人聊到z3，正好在寒假的时候仔细研究过这个模块，今天就和大家分享下z3的简易使用方法和在ctf中该模块对于求解逆向题的帮助</p>
<h1 id="简介"><a href="#简介" class="headerlink" title="简介"></a>简介</h1><h2 id="z3"><a href="#z3" class="headerlink" title="z3"></a>z3</h2><p>z3是由微软公司开发的一个优秀的SMT求解器，它能够检查逻辑表达式的可满足性，通俗的来讲我们可以简单理解为它是一个解方程的计算器</p>
<h2 id="SMT"><a href="#SMT" class="headerlink" title="SMT"></a>SMT</h2><p>SMT即可满足性模理论，它是对一个实际问题求解的特征描述，这些特征就是我们所求解的特征，SMT会使用一个或多个这样的特征描述式求解，再取每一个特征描述式所对应解的交集。</p>
<p>详细关于SMT的理论可以参考：<a href="https://www.cnblogs.com/steven-yang/p/7104068.html" target="_blank" rel="noopener">https://www.cnblogs.com/steven-yang/p/7104068.html</a></p>
<h2 id="基本数据类型"><a href="#基本数据类型" class="headerlink" title="基本数据类型"></a>基本数据类型</h2><p>在Python中使用Z3模块，我们的所求结果一般有以下几种数据类型</p>
<pre><code>Int   #整型

Bool  #布尔型

Array #数组

BitVec(&apos;a&apos;,8) #char型
</code></pre><p>其中BitVec可以是特定大小的数据类型，不一定是8，例如C语言中的int型可以用BitVec(‘a’,32)表示</p>
<h2 id="基本语句"><a href="#基本语句" class="headerlink" title="基本语句"></a>基本语句</h2><p>在Python中使用该模块，我们通常用到如下几个语句</p>
<p><strong>Solver()</strong></p>
<p>Solver()命令会创建一个通用求解器，创建后我们可以添加我们的约束条件，进行下一步的求解</p>
<p><strong>add()</strong></p>
<p>add()命令用来添加约束条件，通常在solver()命令之后，添加的约束条件通常是一个逻辑等式</p>
<p><strong>check()</strong></p>
<p>该函数通常用来判断在添加完约束条件后，来检测解的情况，有解的时候会回显sat，无解的时候会回显unsat</p>
<p><strong>model()</strong></p>
<p>在存在解的时候，该函数会将每个限制条件所对应的解集的交集，进而得出正解。</p>
<h2 id="模块安装"><a href="#模块安装" class="headerlink" title="模块安装"></a>模块安装</h2><p>linux下可用如下命令：</p>
<pre><code>git clone https://github.com/Z3Prover/z3.git

cd z3

python scripts/mk_make.py

cd build

make

make install
</code></pre><h1 id="z3的简单使用"><a href="#z3的简单使用" class="headerlink" title="z3的简单使用"></a>z3的简单使用</h1><h2 id="求解流程"><a href="#求解流程" class="headerlink" title="求解流程"></a>求解流程</h2><p>上文提到我们可以将z3理解为一个解方程的计算器，对于求解方程，我们通常会经历四个步骤：设未知数，列方程，解方程，得到正解</p>
<p>使用z3模块，在我的眼中也是同我们解方程一样需要经历四个步骤，下面我们简单来看一下</p>
<p>假设有方程组：</p>
<pre><code>30x+15y=675

12x+5y=265
</code></pre><p>我们使用z3来解这个方程组：</p>
<p><strong>1.设未知数</strong></p>
<pre><code>In [1]: from z3 import *

In [2]: x = Real(&apos;x&apos;)

In [3]: y = Real(&apos;y&apos;)
</code></pre><p><strong>2.列方程</strong></p>
<pre><code>In [4]: s = Solver()

In [5]: s.add(30*x+15*y==675)

In [6]: s.add(12*x+5*y==265)
</code></pre><p><strong>3.判断方程解的情况并解方程</strong></p>
<pre><code>In [7]: s.check()
Out[7]: sat

In [8]: result = s.model()
</code></pre><p><strong>4.得出正解</strong></p>
<pre><code>In [9]: print result
[y = 5, x = 20]
</code></pre><p>在交互环境中，我们的求解过程如图</p>
<p><img src="https://i.loli.net/2019/04/06/5ca80a3429c22.jpg" alt="5.jpg"></p>
<p>最终完整的代码如下：</p>
<pre><code>from z3 import *

x = Real(&apos;x&apos;)
y = Real(&apos;y&apos;)

s = Solver()
s.add(30*x+15*y==675)
s.add(12*x+5*y==265)

if s.check() == sat:
    result = s.model()
    print result
else:
    print &apos;no result&apos;
</code></pre><p>可以看到我们很轻松的得到了方程组的解</p>
<p><img src="https://i.loli.net/2019/04/06/5ca80aced6bf2.jpg" alt="6.jpg"></p>
<h2 id="利用z3解逻辑算数题"><a href="#利用z3解逻辑算数题" class="headerlink" title="利用z3解逻辑算数题"></a>利用z3解逻辑算数题</h2><p>可能上面解方程组大家觉得这个模块给我们带来的方便并没有那么大，那么通过下面的题目我们或许会对z3有一个全新的认识</p>
<p>在网上翻了很多题目，最终我找到了15年的一道公务员考试题</p>
<p><img src="https://i.loli.net/2019/04/06/5ca80d2aac914.jpg" alt="7.jpg"></p>
<p>这个问题的逻辑稍显复杂，我们现在用z3做一下，同样也需要经历上面四个步骤：设，列，解，得</p>
<p>设：2014年小李年龄：a，小李弟弟年龄：b，小王年龄：c，小王哥哥年龄：d</p>
<p>节省篇幅，直接写出求解代码：</p>
<pre><code>from z3 import *
a = Real(&apos;a&apos;)
b = Real(&apos;b&apos;)
c = Real(&apos;c&apos;)
d = Real(&apos;d&apos;)

s = Solver()
s.add(b+2==a)
s.add(c+2==d)
s.add(a+5==d)
s.add(b+c-20-20==15)

if s.check()==sat:
    print s.model()
else:
    print &quot;no result&quot;
</code></pre><p>运行结果：</p>
<p><img src="https://i.loli.net/2019/04/06/5ca810dd35daf.jpg" alt="8.jpg"></p>
<p>可以看到我们仅用几行代码就得出了答案，如果用普通的解法，我们要算4个方程所组成的方程组，所以使用z3有时候会大大增加我们的计算效率，简化我们的计算步骤。</p>
<h1 id="z3在逆向题目中的应用"><a href="#z3在逆向题目中的应用" class="headerlink" title="z3在逆向题目中的应用"></a>z3在逆向题目中的应用</h1><p>本篇以ISCC2018的一道RE题目为例，题目名为：My math is bad</p>
<p>将文件拖入ida中定位到main函数，F5反编译</p>
<p><img src="https://i.loli.net/2019/04/06/5ca8138baa122.jpg" alt="9.jpg"></p>
<p>可以看到有一个if判断，猜测if中的函数为关键函数，进入该函数</p>
<p><img src="https://i.loli.net/2019/04/06/5ca81401ead52.jpg" alt="10.jpg"></p>
<p>在这里看到了rand()函数，这是一个生成伪随机数的函数，所以我们几乎不可能通过逆向的方式，来将flag计算出来，继续阅读代码，发现该随机数种子是固定的，我们可以将种子计算出来，这样就可以进而获得系统生成的随机数，在计算种子的时候，我们可以使用z3模块</p>
<p>为了增加可读性，将关键函数的反汇编代码修饰一下：</p>
<pre><code>  __int64 v1; // ST40_8
  __int64 v2; // ST48_8
  __int64 v3; // [rsp+20h] [rbp-60h]
  __int64 v4; // [rsp+28h] [rbp-58h]
  __int64 v5; // [rsp+30h] [rbp-50h]
  __int64 v6; // [rsp+38h] [rbp-48h]
  __int64 v7; // [rsp+50h] [rbp-30h]
  __int64 v8; // [rsp+58h] [rbp-28h]
  __int64 v9; // [rsp+60h] [rbp-20h]
  __int64 v10; // [rsp+68h] [rbp-18h]
  __int64 v11; // [rsp+70h] [rbp-10h]
  __int64 v12; // [rsp+78h] [rbp-8h]

  if ( strlen(s) != 32 )
    return 0LL;
  v3 = unk_6020B0;
  v4 = unk_6020B4;
  v5 = unk_6020B8;
  v6 = unk_6020BC;
  if ( a * *s - b * c != 2652042832920173142LL )
    goto LABEL_15;
  if ( 3LL * c + 4LL * b - a - 2LL * *s != 397958918 )
    goto LABEL_15;
  if ( 3 * *s * b - c * a != 3345692380376715070LL )
    goto LABEL_15;
  if ( 27LL * a + *s - 11LL * b - c != 40179413815LL )
    goto LABEL_15;
  srand(c ^ a ^ *s ^ b);
  v1 = rand() % 50;
  v2 = rand() % 50;
  v7 = rand() % 50;
  v8 = rand() % 50;
  v9 = rand() % 50;
  v10 = rand() % 50;
  v11 = rand() % 50;
  v12 = rand() % 50;
  if ( v6 * v2 + v3 * v1 - v4 - v5 != 61799700179LL
    || v6 + v3 + v5 * v8 - v4 * v7 != 48753725643LL
    || v3 * v9 + v4 * v10 - v5 - v6 != 59322698861LL
    || v5 * v12 + v3 - v4 - v6 * v11 != 51664230587LL )
  {
LABEL_15:
    result = 0LL;
  }
  else
  {
    result = 1LL;
  }
  return result;
}
</code></pre><p>首先我们来计算下a,s,b,c的值：</p>
<pre><code>from z3 import *
a = Int(&apos;a&apos;)
b = Int(&apos;b&apos;)
s = Int(&apos;s&apos;)
c = Int(&apos;c&apos;)

l = Solver()
l.add(a*s-b*c==2652042832920173142)
l.add(3*c+4*b-a-2*s==397958918)
l.add(3 *s * b - c * a == 3345692380376715070)
l.add(27 * a + s - 11 * b - c == 40179413815)

if l.check()==sat:
    print l.model()
else:
    print &apos;no result&apos;
</code></pre><p><img src="https://i.loli.net/2019/04/06/5ca81ccc941ff.jpg" alt="11.jpg"></p>
<p>然后我们计算出srand(c ^ a ^ *s ^ b);中c^a^s^b的值</p>
<pre><code>c = 829124174
b = 862734414
s = 1869639009
a = 1801073242
result = a^b^c^s
print result
</code></pre><p>result的值为103643451</p>
<p>接下来我们继续跟进程序流程，计算rand函数所生成的几个值</p>
<p><img src="https://i.loli.net/2019/04/06/5ca82e010c4ae.jpg" alt="12.jpg"></p>
<p>使用ida动态调试程序，跳转到srand()函数，因为是直接跳过来的，srand()还没有参数，而刚才我们已将该参数的值通过z3计算了出来，所以在程序运行到mov     edi, eax时，直接将eax的值改为103643451即可</p>
<p>然后我们跟进程序，得到了v1的值</p>
<p><img src="https://i.loli.net/2019/04/06/5ca82ffb172a5.jpg" alt="14.jpg"></p>
<p>继续跟进获得了下面的几个生成值</p>
<pre><code>v1 = 0x16
v2 = 0x27
v7 = 0x2d
v8=  0x2d
v9 = 0x23 
v10= 0x29 
v11 = 0xd
v12 = 0x24
</code></pre><p>接着我们到了if的判断</p>
<p><img src="https://i.loli.net/2019/04/06/5ca83192d0a23.jpg" alt="15.jpg"></p>
<p>其中v3 v4 v5 v6是未知的，所以在这里我们可以设四个未知数，其他数我们通过前面已经计算出来了，使用z3求解这四个未知数即可</p>
<pre><code>from z3 import *
v3 = Int(&apos;v3&apos;)
v4 = Int(&apos;v4&apos;)
v5 = Int(&apos;v5&apos;)
v6 = Int(&apos;v6&apos;)
v1 = 0x16
v2 = 0x27
v7 = 0x2d
v8=  0x2d
v9 = 0x23
v10= 0x29
v11 = 0xd
v12 = 0x24

l = Solver()
l.add(v6 * v2 + v3 * v1 - v4 - v5 == 61799700179)
l.add(v6 + v3 + v5 * v8 - v4 * v7 == 48753725643)
l.add(v3 * v9 + v4 * v10 - v5 - v6 == 59322698861)
l.add(v5 * v12 + v3 - v4 - v6 * v11 == 51664230587)

if l.check() == sat:
    print l.model()
else:
    print &apos;no result&apos;
</code></pre><p>运行结果</p>
<p><img src="https://i.loli.net/2019/04/06/5ca8328b64699.jpg" alt="16.jpg"></p>
<p>至此我们需要输入的值都计算出来了</p>
<pre><code>c = 829124174
b = 862734414
s = 1869639009
a = 1801073242
v6 = 1195788129
v4 = 828593230
v3 = 811816014
v5 = 1867395930
</code></pre><p>这里我们需要将abcs的顺序确定一下，在bss段中可看到其顺序</p>
<p><img src="https://i.loli.net/2019/04/06/5ca834ef90a97.jpg" alt="17.jpg"></p>
<p>然后我们需要将这些数字转换为字符串输入，这里用到了libnum库</p>
<pre><code>import libnum
c = 829124174
b = 862734414
s = 1869639009
a = 1801073242
v6 = 1195788129
v4 = 828593230
v3 = 811816014
v5 = 1867395930

array = [s,a,c,b,v3,v4,v5,v6]
result = &quot;&quot;
for i in array:
    result = result + libnum.n2s(i)[::-1]
print result
</code></pre><p>运行脚本</p>
<p><img src="https://i.loli.net/2019/04/06/5ca8395b629d4.jpg" alt="18.jpg"></p>
<p>将字符串输入后我们即可得到flag</p>
<p><img src="https://i.loli.net/2019/04/06/5ca839bde9e02.jpg" alt="19.jpg"></p>
<h1 id="总结"><a href="#总结" class="headerlink" title="总结"></a>总结</h1><p>z3是一个强大的约束求解器，它不仅能处理一些看起来很复杂的逻辑问题，在逆向领域中往往可以简化我们计算步骤，增加求解效率，尤其是在ctf比赛中一些繁杂的RE题目通过z3来解往往显得非常简单，我们在解决问题时如果能灵活应用z3，往往会有意想不到的效果。</p>

      
    </div>
    
    
    

    

    
      <div>
        <div style="padding: 10px 0; margin: 20px auto; width: 90%; text-align: center;">
  <div>坚持原创技术分享，您的支持将鼓励我继续创作！</div>
  <button id="rewardButton" disable="enable" onclick="var qr = document.getElementById('QR'); if (qr.style.display === 'none') {qr.style.display='block';} else {qr.style.display='none'}">
    <span>Donate</span>
  </button>
  <div id="QR" style="display: none;">

    
      <div id="wechat" style="display: inline-block">
        <img id="wechat_qr" src="/images/wechatpay.jpg" alt="夜莫离、 WeChat Pay">
        <p>WeChat Pay</p>
      </div>
    

    
      <div id="alipay" style="display: inline-block">
        <img id="alipay_qr" src="/images/alipay.jpg" alt="夜莫离、 Alipay">
        <p>Alipay</p>
      </div>
    

    

  </div>
</div>

      </div>
    

    

    <footer class="post-footer">
      
        <div class="post-tags">
          
            <a href="/tags/系统总结/" rel="tag"># 系统总结</a>
          
        </div>
      

      
      
      

      
        <div class="post-nav">
          <div class="post-nav-next post-nav-item">
            
              <a href="/2019/04/01/2019嘉韦思杯线上赛wp/" rel="next" title="2019嘉韦思杯线上赛wp">
                <i class="fa fa-chevron-left"></i> 2019嘉韦思杯线上赛wp
              </a>
            
          </div>

          <span class="post-nav-divider"></span>

          <div class="post-nav-prev post-nav-item">
            
              <a href="/2019/04/26/newbugku部分web题解/" rel="prev" title="newbugku部分web题解">
                newbugku部分web题解 <i class="fa fa-chevron-right"></i>
              </a>
            
          </div>
        </div>
      

      
      
    </footer>
  </div>
  
  
  
  </article>



    <div class="post-spread">
      
    </div>
  </div>


          </div>
          


          

  



        </div>
        
          
  
  <div class="sidebar-toggle">
    <div class="sidebar-toggle-line-wrap">
      <span class="sidebar-toggle-line sidebar-toggle-line-first"></span>
      <span class="sidebar-toggle-line sidebar-toggle-line-middle"></span>
      <span class="sidebar-toggle-line sidebar-toggle-line-last"></span>
    </div>
  </div>

  <aside id="sidebar" class="sidebar">
    
    <div class="sidebar-inner">

      

      
        <ul class="sidebar-nav motion-element">
          <li class="sidebar-nav-toc sidebar-nav-active" data-target="post-toc-wrap">
            Table of Contents
          </li>
          <li class="sidebar-nav-overview" data-target="site-overview-wrap">
            Overview
          </li>
        </ul>
      

      <section class="site-overview-wrap sidebar-panel">
        <div class="site-overview">
          <div class="site-author motion-element" itemprop="author" itemscope="" itemtype="http://schema.org/Person">
            
              <p class="site-author-name" itemprop="name">夜莫离、</p>
              <p class="site-description motion-element" itemprop="description"></p>
          </div>

          <nav class="site-state motion-element">

            
              <div class="site-state-item site-state-posts">
              
                <a href="/archives/">
              
                  <span class="site-state-item-count">58</span>
                  <span class="site-state-item-name">posts</span>
                </a>
              </div>
            

            

            
              
              
              <div class="site-state-item site-state-tags">
                <a href="/tags/index.html">
                  <span class="site-state-item-count">16</span>
                  <span class="site-state-item-name">tags</span>
                </a>
              </div>
            

          </nav>

          

          
            <div class="links-of-author motion-element">
                
                  <span class="links-of-author-item">
                    <a href="https://github.com/yemoli" target="_blank" title="GitHub">
                      
                        <i class="fa fa-fw fa-github"></i>GitHub</a>
                  </span>
                
            </div>
          

          
          

          
          
            <div class="links-of-blogroll motion-element links-of-blogroll-block">
              <div class="links-of-blogroll-title">
                <i class="fa  fa-fw fa-link"></i>
                Links
              </div>
              <ul class="links-of-blogroll-list">
                
                  <li class="links-of-blogroll-item">
                    <a href="https://chxing.xyz/" title="Bling_Dog" target="_blank">Bling_Dog</a>
                  </li>
                
                  <li class="links-of-blogroll-item">
                    <a href="https://www.smi1e.top/" title="Smi1e" target="_blank">Smi1e</a>
                  </li>
                
                  <li class="links-of-blogroll-item">
                    <a href="https://altman.vip/" title="Altman" target="_blank">Altman</a>
                  </li>
                
                  <li class="links-of-blogroll-item">
                    <a href="https://www.virtua1.cn/" title="Virtua1" target="_blank">Virtua1</a>
                  </li>
                
                  <li class="links-of-blogroll-item">
                    <a href="https://www.zhaoj.in/" title="赵" target="_blank">赵</a>
                  </li>
                
                  <li class="links-of-blogroll-item">
                    <a href="http://www.dongzt.cn/" title="Alkaid" target="_blank">Alkaid</a>
                  </li>
                
                  <li class="links-of-blogroll-item">
                    <a href="https://cdusec.com/" title="CDUSEC" target="_blank">CDUSEC</a>
                  </li>
                
                  <li class="links-of-blogroll-item">
                    <a href="http://cdusec.happyhacking.top/" title="CDUSEC内部博客" target="_blank">CDUSEC内部博客</a>
                  </li>
                
                  <li class="links-of-blogroll-item">
                    <a href="http://jjhpkcr.xyz/" title="江江河畔砍柴人" target="_blank">江江河畔砍柴人</a>
                  </li>
                
                  <li class="links-of-blogroll-item">
                    <a href="http://www.youknowi.xin/" title="图先生" target="_blank">图先生</a>
                  </li>
                
                  <li class="links-of-blogroll-item">
                    <a href="https://a3ura.github.io/" title="a3ura" target="_blank">a3ura</a>
                  </li>
                
                  <li class="links-of-blogroll-item">
                    <a href="http://www.recorday.cn/" title="C0d3r1iu" target="_blank">C0d3r1iu</a>
                  </li>
                
                  <li class="links-of-blogroll-item">
                    <a href="https://www.iloveflag.com/" title="醉梦半醒" target="_blank">醉梦半醒</a>
                  </li>
                
              </ul>
            </div>
          

          

        </div>
      </section>

      
      <!--noindex-->
        <section class="post-toc-wrap motion-element sidebar-panel sidebar-panel-active">
          <div class="post-toc">

            
              
            

            
              <div class="post-toc-content"><ol class="nav"><li class="nav-item nav-level-1"><a class="nav-link" href="#简介"><span class="nav-number">1.</span> <span class="nav-text">简介</span></a><ol class="nav-child"><li class="nav-item nav-level-2"><a class="nav-link" href="#z3"><span class="nav-number">1.1.</span> <span class="nav-text">z3</span></a></li><li class="nav-item nav-level-2"><a class="nav-link" href="#SMT"><span class="nav-number">1.2.</span> <span class="nav-text">SMT</span></a></li><li class="nav-item nav-level-2"><a class="nav-link" href="#基本数据类型"><span class="nav-number">1.3.</span> <span class="nav-text">基本数据类型</span></a></li><li class="nav-item nav-level-2"><a class="nav-link" href="#基本语句"><span class="nav-number">1.4.</span> <span class="nav-text">基本语句</span></a></li><li class="nav-item nav-level-2"><a class="nav-link" href="#模块安装"><span class="nav-number">1.5.</span> <span class="nav-text">模块安装</span></a></li></ol></li><li class="nav-item nav-level-1"><a class="nav-link" href="#z3的简单使用"><span class="nav-number">2.</span> <span class="nav-text">z3的简单使用</span></a><ol class="nav-child"><li class="nav-item nav-level-2"><a class="nav-link" href="#求解流程"><span class="nav-number">2.1.</span> <span class="nav-text">求解流程</span></a></li><li class="nav-item nav-level-2"><a class="nav-link" href="#利用z3解逻辑算数题"><span class="nav-number">2.2.</span> <span class="nav-text">利用z3解逻辑算数题</span></a></li></ol></li><li class="nav-item nav-level-1"><a class="nav-link" href="#z3在逆向题目中的应用"><span class="nav-number">3.</span> <span class="nav-text">z3在逆向题目中的应用</span></a></li><li class="nav-item nav-level-1"><a class="nav-link" href="#总结"><span class="nav-number">4.</span> <span class="nav-text">总结</span></a></li></ol></div>
            

          </div>
        </section>
      <!--/noindex-->
      

      

    </div>
  </aside>


        
      </div>
    </main>

    <footer id="footer" class="footer">
      <div class="footer-inner">
        <div class="copyright">&copy; 2018 &mdash; <span itemprop="copyrightYear">2020</span>
  <span class="with-love">
    <i class="fa fa-user"></i>
  </span>
  <span class="author" itemprop="copyrightHolder">夜莫离、</span>

  
</div>


  <!-- <div class="powered-by">Powered by <a class="theme-link" target="_blank" href="https://hexo.io">Hexo</a></div> 



  <span class="post-meta-divider">|</span>



  <div class="theme-info">Theme &mdash; <a class="theme-link" target="_blank" href="https://github.com/iissnan/hexo-theme-next">NexT.Mist</a> v5.1.4</div>-->



<div class="theme-info">
 <div class="powered-by"></div>
 <span class="post-count">博客全站共63.1k字</span>
</div>
        







        
      </div>
    </footer>

    
      <div class="back-to-top">
        <i class="fa fa-arrow-up"></i>
        
      </div>
    

    

  </div>

  

<script type="text/javascript">
  if (Object.prototype.toString.call(window.Promise) !== '[object Function]') {
    window.Promise = null;
  }
</script>









  


  











  
  
    <script type="text/javascript" src="/lib/jquery/index.js?v=2.1.3"></script>
  

  
  
    <script type="text/javascript" src="/lib/fastclick/lib/fastclick.min.js?v=1.0.6"></script>
  

  
  
    <script type="text/javascript" src="/lib/jquery_lazyload/jquery.lazyload.js?v=1.9.7"></script>
  

  
  
    <script type="text/javascript" src="/lib/velocity/velocity.min.js?v=1.2.1"></script>
  

  
  
    <script type="text/javascript" src="/lib/velocity/velocity.ui.min.js?v=1.2.1"></script>
  

  
  
    <script type="text/javascript" src="/lib/fancybox/source/jquery.fancybox.pack.js?v=2.1.5"></script>
  

  
  
    <script type="text/javascript" src="/lib/canvas-nest/canvas-nest.min.js"></script>
  


  


  <script type="text/javascript" src="/js/src/utils.js?v=5.1.4"></script>

  <script type="text/javascript" src="/js/src/motion.js?v=5.1.4"></script>



  
  

  
  <script type="text/javascript" src="/js/src/scrollspy.js?v=5.1.4"></script>
<script type="text/javascript" src="/js/src/post-details.js?v=5.1.4"></script>



  


  <script type="text/javascript" src="/js/src/bootstrap.js?v=5.1.4"></script>



  


  




	





  





  












  





  

  

  

  
  

  

  

  

  
<script type="text/javascript" src="//cdn.bootcss.com/canvas-nest.js/1.0.0/canvas-nest.min.js"></script>

<!-- 页面点击小红心 -->
<script type="text/javascript" src="/js/src/love.js"></script>
</body>
</html>
